Model checking decides the problem of whether a system satisfies a temporal logic property by exploring the underlying state space. It applies primarily to finite-state models or systems (FSMs) where all the execution paths are infinite. However it can also be conducted on FSMs where some of the execution paths are finite. The state space can be represented in symbolic or explicit form. Symbolic model checking has traditionally employed a Boolean representation of state sets using binary decision diagrams (BDDs) as a way of checking temporal properties, whereas explicit-state model checkers enumerate the set of reachable states of the system.
A path is a maximal sequence of states (S0, S1, S2, . . . ) such that S0 is an initial state and for each two consecutive states (Si−1,Si) there is a transition from state Si−1 to state Si. The path is infinite if this sequence is infinite. The path is finite if this sequence is finite (i.e., there is no outgoing transition from the last state in this sequence). A bounded path is an initial portion of a path of length n, also known as a “prefix” of a path, and is finite.
Reference is now made to FIG. 1, which illustrates a simple, finite state machine of four states (1-4), where the initial state is 4. In the state machine of FIG. 1, there are transitions (indicated by arrows) back and forth from state 2 to each of the other states 1, 3 and 4. In addition, there is a self-loop labeled 8 at state 1. The transition relation in the state machine in FIG. 1 is total (i.e. there is always a transition from one state to another) and therefore, all the paths are infinite paths. For example, there is a path from state 4 to state 2 to state 4 to state 2, etc. If the path passes through state 1, it can either stay at state 1 (via self-loop 8) or it may return to state 2.
In the article, Symbolic Model Checking without BDDs, by Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu in TACAS 1999, the use of Boolean satisfiability (SAT) solvers for linear-time temporal logic (LTL) properties was explored through a technique known as bounded model checking (BMC). As with symbolic model checking, in bounded model checking, the state is encoded in terms of Booleans. A bounded model checker unrolls the model a bounded number of steps for some bound k, and prepares a translation of the model to be checked with a SAT solver for counterexamples over computations of length k.
The translation being checked is defined as the question, is there a bounded path of length k that contains a bug, where a bug is defined as a Boolean predicate over the state of the FSM. If the translation is satisfied (i.e. the answer to the question is Yes), then there is a bug in the model being checked.
A translation A is defined mathematically as:
                    A        =                              INIT            ⁡                          (                              S                0                            )                                ⋀                      (                                          ⋀                                  i                  =                  1                                k                            ⁢                              TR                ⁡                                  (                                                            S                                              i                        -                        1                                                              ,                                          S                      i                                                        )                                                      )                    ⋀                      (                                          ⋁                                  i                  =                  0                                k                            ⁢                              BAD                ⁡                                  (                                      S                    i                                    )                                                      )                                              (        1        )            where INIT, TR and BAD are Boolean predicates which check the status of the variables on which they operate. INIT(S0) returns True if state S0 is one of the initial states, TR(Si−1,Si) returns True if transition (Si−1,Si) is a valid transition of the finite state machine and BAD(Si) returns True if state Si is a non-allowed value (i.e. that indicates a bug).
Equation 1 indicates that there is a bounded path of length k such that S0 is in the initial set INIT(S0), for each two consecutive states (Si−1,Si) there is a transition from state Si−1 to state Si and the bounded path passes through a bad state.
The SAT solver then attempts to satisfy condition A (i.e. to find a valid bounded path to at least one of the states that satisfies BAD). A bug is defined as a bad state that is reachable by a computation path. The SAT solver typically also generates a counter-example trace leading to the bug.
In practice, the verification engineer fixes the length parameter k, for example, k=10. The bounded model checker produces translation A and provides it to the SAT solver. If the SAT solver determines that the translation is satisfiable, then a bug is found; otherwise, the result is seen as “k-passed” (i.e. the model does not contain a bug on any bounded path up to length k). Some modern verification tools, such as RuleBase, commercially available from International Business Machines (IBM) Corporation of the USA, also provide automatic modes in which the bound k is automatically increased until a bug is found or the system runs out of resources.